Nuprl Lemma : Rusends1_wf
11,40
postcript
pdf
k
:Knd,
l
:IdLnk,
ds
:
x
:Id fp
Type,
A
,
T
:Type,
tg
:Id,
f
:(State(
ds
)
A
T
).
k
(v) sends [
tg
,
f
(State(
ds
), v)] on
l
Realizer
latex
Definitions
x
.
t
(
x
)
,
Top
,
DeclaredType(
ds
;
x
)
,
k
(v) sends [
tg
,
f
(State(
ds
), v)] on
l
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
Lemmas
Knd
wf
,
IdLnk
wf
,
fpf
wf
,
Id
wf
,
decl-state
wf
,
decl-type
wf
,
id-deq
wf
,
fpf-cap-single1
,
Rsends
wf
,
fpf-single
wf3
origin
k:Knd, l:IdLnk, ds:x:Id fp
Type, A, T:Type, tg:Id, f:(State(ds)
AT).
Realizer k:Knd, l:IdLnk, ds:x:Id fp Type, A, T:Type, tg:Id, f:(State(ds)AT).
Realizer 
x. t(x) Tx:A. B(x)